"""
SMT2/BTOR model parsers that extract structural metrics and validate basic syntax - the validation is really primitive and fragile.

Key Features:
- SMT2ModelParser: Analyzes command distribution, line types, and Rotor metadata
- BTORModelParser: Placeholder for future BTOR format support
- Strict validation against SMT-LIBv2 specifications
"""

from lib.paths import OutputPath
from lib.rotor_parser import SMT2RotorParser
from lib.model_data import ParsedSMT2ModelData
from lib.exceptions import ParsingError

from abc import ABC, abstractmethod
import re


class ModelParser:
    """Abstract base class for model format parsers."""
    def __init__(self, model_path: OutputPath):
        self.model_path = model_path

    @abstractmethod
    def parse(self):
        pass

    @abstractmethod
    def log(self):
        pass


class SMT2ModelParser(ModelParser):
    """Parses SMT-LIBv2 files (with Rotor-specific extensions for Rotor generated models)"""
    def __init__(self, model_path: OutputPath):
        super().__init__(model_path)
        self.rotor_header: "RotorModelData" = None
        self.parsed_data: ParsedSMT2ModelData = ParsedSMT2ModelData()

    def parse(self):
        """
        Analyzes an SMT-LIBv2 file and returns statistics.

        It will raise an error if invalid SMT-LIBv2 has been provided.
        Invalid SMT-LIBv2 file:
        A strictly compliant SMT-LIB v2 file cannot have anything other than:

            (commands)

            ;comments

            whitespace (spaces, newlines, etc.)
        """

        # Regex patterns
        comment_pattern = re.compile(r"^\s*;")
        blank_pattern = re.compile(r"^\s*$")
        line_pattern = re.compile(r"^\s*\(.*\)\s*$")

        define_pattern = re.compile(r"^\s*\(define", re.IGNORECASE)
        declare_pattern = re.compile(r"^\s*\(declare", re.IGNORECASE)
        assertion_pattern = re.compile(r"^\s*\(assert", re.IGNORECASE)
        push_pattern = re.compile(r"^\s*\(push", re.IGNORECASE)
        pop_pattern = re.compile(r"^\s*\(pop", re.IGNORECASE)
        check_sat_pattern = re.compile(r"^\s*\(check-sat", re.IGNORECASE)

        # Model generated by rotor have this signature pattern
        self.rotor_signature = re.compile(
            r"^;\s*generated\s+SMT-LIB\s+file\s+(.+\.smt2)"
        )
        previous_command = None

        with open(self.model_path, "r") as f:
            for line in f:
                # Check for rotor signature first
                if (
                    not self.parsed_data.is_rotor_generated
                    and self.rotor_signature.match(line)
                ):
                    self.parsed_data.is_rotor_generated = True
                    self.parsed_data.rotor_data = SMT2RotorParser.parse_header(
                        self.model_path
                    )

                self.parsed_data.total_lines += 1

                if comment_pattern.match(line):
                    self.parsed_data.comment_lines += 1
                elif blank_pattern.match(line):
                    self.parsed_data.blank_lines += 1
                elif line_pattern.match(line):
                    self.parsed_data.code_lines += 1

                    # Check for specific lines
                    if define_pattern.search(line):
                        self.parsed_data.definition += 1
                    elif declare_pattern.search(line):
                        self.parsed_data.declaration += 1
                    elif assertion_pattern.search(line):
                        self.parsed_data.assertion += 1
                    elif push_pattern.search(line):
                        self.parsed_data.push += 1
                    elif pop_pattern.search(line):
                        self.parsed_data.pop += 1
                    elif check_sat_pattern.search(line):
                        self.parsed_data.check_sat += 1
                    else:
                        self.parsed_data.other_commands += 1
                else:
                    raise ParsingError(self.model_path, line, line)

        return self.parsed_data


class BTORModelParser(ModelParser):
    """Placeholder for future BTOR format parsing."""
    def __init__(self, output_path: OutputPath):
        super().__init__(output_path)

    def parse(self):
        pass

    def log(self):
        pass
